Nuprl Lemma : es_realizer_ind_wf 0,22
X:Type{j}, x1:es_realizer{i:l}, none:X, plus:(es_realizer{i:l}es_realizer{i:l}XXX),
init:(Id(T:Type{i}IdTX)), frame:(IdType{i}Id(Knd List)X),
sframe:(IdLnkId(Knd List)X),
effect:(Id(ds:x:Id fp Type{i}Knd(T:Type{i}x:Id(State(ds)Tdecl-type{i:l}(ds; x))
effect:(Id(ds:x:Id fp Type{i}Knd(X))),
sends:(ds:x:Id fp Type{i}Knd
sends:((T:Type{i}IdLnk(dt:x:Id fp Type{i}((tg:Id
sends:((T:Type{i}IdLnk(dt:x:Id fp Type{i}(((State(ds)T(decl-type{i:l}
sends:((T:Type{i}IdLnk(dt:x:Id fp Type{i}(((State(ds)T(decl-type(dt; tg) List))) List)
sends:((T:Type{i}IdLnk(X))),
pre:(Id(ds:x:Id fp Type{i}Id(T:Type{i}(State(ds)TProp{i})X))),
aframe:(IdKnd(Id List)X), bframe:(IdKnd(IdLnk List)X), rframe:(IdId(Knd List)X).
case x1 of 
Rnone => none
Rplus(left,right)=>rec1,rec2.plus(left,right,rec1,rec2)
Rinit(loc,T,x,v)=> init(loc,T,x,v)
Rframe(loc,T,x,L)=> frame(loc,T,x,L)
Rsframe(lnk,tag,L)=> sframe(lnk,tag,L)
Reffect(loc,ds,knd,T,x,f)=> effect(loc,ds,knd,T,x,f)
Rsends(ds,knd,T,l,dt,g)=> sends(ds,knd,T,l,dt,g)
Rpre(loc,ds,a,T,P)=> pre(loc,ds,a,T,P)
Raframe(loc,k,L)=> aframe(loc,k,L)
Rbframe(loc,k,L)=> bframe(loc,k,L)
Rrframe(loc,x,L)=> rframe(loc,x,L)
 X 
latex

Definitionsx:A. B(x), Realizer, Prop, t  T, es realizer ind, x(s1,s2,s3,s4), x(s1,s2,s3), x(a,b,c,d,e,f), x(s1,s2,s3,s4,s5), x. t(x), Y, 1of(t), 2of(t), x(s)
Lemmasunit wf, Id wf, Knd wf, IdLnk wf, fpf wf, decl-state wf, decl-type wf, es realizer wf

origin